(set-logic QF_UFLIA)
(set-info :source |
  These benchmarks were obtained from the KIND tool during verification of
  Lustre programs.  See also the lustre family of benchmarks in QF_LIA.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun _base () Int)
(declare-fun _n () Int)
(assert (<= 0 _n))
(declare-fun ___z2z___ (Int) Bool)
(declare-fun ___z3z___ (Int) Bool)
(declare-fun ___z4z___ (Int) Bool)
(declare-fun ___z5z___ (Int) Bool)
(declare-fun ___z6z___ (Int) Bool)
(declare-fun ___z7z___ (Int) Bool)
(declare-fun ___z8z___ (Int) Bool)
(declare-fun ___z9z___ (Int) Bool)
(declare-fun ___z10z___ (Int) Int)
(declare-fun ___z11z___ (Int) Bool)
(declare-fun ___z12z___ (Int) Int)
(declare-fun ___z13z___ (Int) Int)
(declare-fun ___z14z___ (Int) Int)
(declare-fun ___z15z___ (Int) Int)
(declare-fun ___z16z___ (Int) Bool)
(declare-fun ___z17z___ (Int) Bool)
(declare-fun ___z18z___ (Int) Bool)
(declare-fun ___z19z___ (Int) Bool)
(declare-fun ___z20z___ (Int) Bool)
(declare-fun ___z21z___ (Int) Bool)
(declare-fun ___z22z___ (Int) Bool)
(declare-fun ___z23z___ (Int) Bool)
(declare-fun ___z24z___ (Int) Bool)
(declare-fun ___z25z___ (Int) Int)
(declare-fun ___z26z___ (Int) Bool)
(declare-fun ___z27z___ (Int) Int)
(push 1)
(assert (= (<= 1 (___z14z___ (- 1))) (___z20z___ 0)))
(assert (= (or (not (___z16z___ 0)) (= (+ (___z27z___ 0) (+ (* (- 1) (___z15z___ 0)) (+ (* (- 1) (___z14z___ 0)) (+ (* (- 1) (___z13z___ 0)) (* (- 1) (___z12z___ 0)))))) 0)) (___z11z___ 0)))
(assert (= (= (___z15z___ (- 1)) 1) (___z21z___ 0)))
(assert (let ((?v_0 (___z12z___ (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ 0) (ite (= _base 0) (___z25z___ 0) (ite (___z2z___ 0) (ite (___z17z___ 0) ?v_1 ?v_0) (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) ?v_1 ?v_0) (ite (___z7z___ 0) (ite (___z22z___ 0) ?v_1 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) ?v_1 ?v_0) ?v_0)))))))))))
(assert (= (___z22z___ 0) (and (= (___z14z___ (- 1)) 0) (and (= (___z15z___ (- 1)) 0) (and (= (___z13z___ (- 1)) 0) (<= 1 (___z12z___ (- 1))))))))
(assert (let ((?v_0 (___z13z___ (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z5z___ 0) (ite (___z20z___ 0) (+ 1 ?v_0) ?v_0) (ite (___z7z___ 0) (ite (___z22z___ 0) 1 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) ?v_0)))))))))
(assert (= (___z23z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (___z13z___ (- 1))))))
(assert (let ((?v_0 (___z14z___ (- 1)))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ 0) (ite (= _base 0) 0 (ite (___z2z___ 0) (ite (___z17z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) 0 ?v_0) (ite (___z5z___ 0) (ite (___z20z___ 0) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ 0) (ite (___z21z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) 0 ?v_0) ?v_0))))))))))
(assert (= (___z24z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))))))
(assert (let ((?v_2 (___z14z___ (- 1))) (?v_0 (___z15z___ (- 1)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) (+ (- 1) (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ 0) (ite (___z21z___ 0) 0 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0))))))))))
(assert (= (___z25z___ 0) (ite (= _base 0) (___z10z___ 0) (___z25z___ (- 1)))))
(assert (let ((?v_0 (= _base 0)) (?v_1 (___z26z___ 0))) (= (___z16z___ 0) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (___z16z___ (- 1))))))))
(assert (let ((?v_2 (___z9z___ 0)) (?v_0 (___z8z___ 0)) (?v_5 (___z7z___ 0)) (?v_14 (___z4z___ 0)) (?v_17 (___z3z___ 0)) (?v_19 (___z2z___ 0)) (?v_11 (___z5z___ 0)) (?v_8 (___z6z___ 0))) (let ((?v_3 (not ?v_2)) (?v_18 (not ?v_19)) (?v_20 (not ?v_17))) (let ((?v_15 (and ?v_20 ?v_18)) (?v_16 (not ?v_14))) (let ((?v_12 (and ?v_16 ?v_15)) (?v_13 (not ?v_11))) (let ((?v_9 (and ?v_13 ?v_12)) (?v_10 (not ?v_8))) (let ((?v_6 (and ?v_10 ?v_9)) (?v_7 (not ?v_5))) (let ((?v_1 (and ?v_7 ?v_6)) (?v_4 (not ?v_0))) (let ((?v_21 (and ?v_4 ?v_1))) (= (___z26z___ 0) (and (<= 0 (___z10z___ 0)) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3))))))))))))))))))))
(assert (= (___z17z___ 0) (and (= (___z14z___ (- 1)) 0) (and (= (___z15z___ (- 1)) 0) (and (= (___z13z___ (- 1)) 0) (<= 1 (___z12z___ (- 1))))))))
(assert (= (___z27z___ 0) (ite (= _base 0) (___z10z___ 0) (___z27z___ (- 1)))))
(assert (= (___z18z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (___z13z___ (- 1))))))
(assert (= (___z19z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))))))
(assert (= (<= 1 (___z14z___ (- 2))) (___z20z___ (- 1))))
(assert (= (or (not (___z16z___ (- 1))) (= (+ (___z14z___ (- 1)) (+ (___z15z___ (- 1)) (+ (___z12z___ (- 1)) (+ (___z13z___ (- 1)) (* (- 1) (___z27z___ (- 1))))))) 0)) (___z11z___ (- 1))))
(assert (= (= (___z15z___ (- 2)) 1) (___z21z___ (- 1))))
(assert (let ((?v_0 (___z12z___ (- 2)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ (- 1)) (ite (= _base (- 1)) (___z25z___ (- 1)) (ite (___z2z___ (- 1)) (ite (___z17z___ (- 1)) ?v_1 ?v_0) (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) ?v_1 ?v_0) (ite (___z7z___ (- 1)) (ite (___z22z___ (- 1)) ?v_1 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) ?v_1 ?v_0) ?v_0)))))))))))
(assert (= (___z22z___ (- 1)) (and (= (___z14z___ (- 2)) 0) (and (= (___z15z___ (- 2)) 0) (and (= (___z13z___ (- 2)) 0) (<= 1 (___z12z___ (- 2))))))))
(assert (let ((?v_0 (___z13z___ (- 2)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z5z___ (- 1)) (ite (___z20z___ (- 1)) (+ 1 ?v_0) ?v_0) (ite (___z7z___ (- 1)) (ite (___z22z___ (- 1)) 1 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) ?v_0)))))))))
(assert (= (___z23z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (___z13z___ (- 2))))))
(assert (let ((?v_0 (___z14z___ (- 2)))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z2z___ (- 1)) (ite (___z17z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) 0 ?v_0) (ite (___z5z___ (- 1)) (ite (___z20z___ (- 1)) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ (- 1)) (ite (___z21z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) 0 ?v_0) ?v_0))))))))))
(assert (= (___z24z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (+ (___z14z___ (- 2)) (___z15z___ (- 2)))))))
(assert (let ((?v_2 (___z14z___ (- 2))) (?v_0 (___z15z___ (- 2)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) (+ (- 1) (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ (- 1)) (ite (___z21z___ (- 1)) 0 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0))))))))))
(assert (= (___z25z___ (- 1)) (ite (= _base (- 1)) (___z10z___ (- 1)) (___z25z___ (- 2)))))
(assert (let ((?v_0 (= _base (- 1))) (?v_1 (___z26z___ (- 1)))) (= (___z16z___ (- 1)) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (___z16z___ (- 2))))))))
(assert (let ((?v_19 (___z2z___ (- 1))) (?v_17 (___z3z___ (- 1))) (?v_14 (___z4z___ (- 1))) (?v_5 (___z7z___ (- 1))) (?v_0 (___z8z___ (- 1))) (?v_2 (___z9z___ (- 1))) (?v_11 (___z5z___ (- 1))) (?v_8 (___z6z___ (- 1)))) (let ((?v_4 (not ?v_0)) (?v_7 (not ?v_5)) (?v_10 (not ?v_8)) (?v_13 (not ?v_11)) (?v_16 (not ?v_14)) (?v_20 (not ?v_17)) (?v_18 (not ?v_19))) (let ((?v_15 (and ?v_20 ?v_18))) (let ((?v_12 (and ?v_16 ?v_15))) (let ((?v_9 (and ?v_13 ?v_12))) (let ((?v_6 (and ?v_10 ?v_9))) (let ((?v_1 (and ?v_7 ?v_6))) (let ((?v_21 (and ?v_4 ?v_1)) (?v_3 (not ?v_2))) (= (___z26z___ (- 1)) (and (<= 0 (___z10z___ (- 1))) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3))))))))))))))))))))
(assert (= (___z17z___ (- 1)) (and (= (___z14z___ (- 2)) 0) (and (= (___z15z___ (- 2)) 0) (and (= (___z13z___ (- 2)) 0) (<= 1 (___z12z___ (- 2))))))))
(assert (= (___z27z___ (- 1)) (ite (= _base (- 1)) (___z10z___ (- 1)) (___z27z___ (- 2)))))
(assert (= (___z18z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (___z13z___ (- 2))))))
(assert (= (___z19z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (+ (___z14z___ (- 2)) (___z15z___ (- 2)))))))
(push 1)
(assert (not (or (not (= _base (- 1))) (and (___z11z___ 0) (___z11z___ (- 1))))))
(assert true)
(set-info :status unsat)
(check-sat)
(pop 1)
(assert (___z11z___ (- 1)))
(assert (___z11z___ (- 2)))
(push 1)
(assert (= (<= 1 (___z14z___ (+ _n (- 1)))) (___z20z___ _n)))
(assert (= (or (not (___z16z___ _n)) (= (+ (___z27z___ _n) (+ (* (- 1) (___z15z___ _n)) (+ (* (- 1) (___z14z___ _n)) (+ (* (- 1) (___z13z___ _n)) (* (- 1) (___z12z___ _n)))))) 0)) (___z11z___ _n)))
(assert (= (= (___z15z___ (+ _n (- 1))) 1) (___z21z___ _n)))
(assert (let ((?v_0 (___z12z___ (+ _n (- 1))))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ _n) (ite (= _n _base) (___z25z___ _n) (ite (___z2z___ _n) (ite (___z17z___ _n) ?v_1 ?v_0) (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_1 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) ?v_1 ?v_0) (ite (___z7z___ _n) (ite (___z22z___ _n) ?v_1 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_1 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) ?v_1 ?v_0) ?v_0)))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z22z___ _n) (and (= (___z14z___ ?v_0) 0) (and (= (___z15z___ ?v_0) 0) (and (= (___z13z___ ?v_0) 0) (<= 1 (___z12z___ ?v_0))))))))
(assert (let ((?v_0 (___z13z___ (+ _n (- 1))))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ _n) (ite (= _n _base) 0 (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_1 ?v_0) (ite (___z5z___ _n) (ite (___z20z___ _n) (+ 1 ?v_0) ?v_0) (ite (___z7z___ _n) (ite (___z22z___ _n) 1 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_1 ?v_0) ?v_0)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z23z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (___z13z___ ?v_0))))))
(assert (let ((?v_0 (___z14z___ (+ _n (- 1))))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ _n) (ite (= _n _base) 0 (ite (___z2z___ _n) (ite (___z17z___ _n) ?v_1 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) 0 ?v_0) (ite (___z5z___ _n) (ite (___z20z___ _n) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ _n) (ite (___z21z___ _n) ?v_1 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) 0 ?v_0) ?v_0))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z24z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (+ (___z14z___ ?v_0) (___z15z___ ?v_0)))))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_3 (___z14z___ ?v_1)) (?v_0 (___z15z___ ?v_1))) (let ((?v_2 (+ 2 ?v_0))) (= (___z15z___ _n) (ite (= _n _base) 0 (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_2 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) (+ (- 1) (+ ?v_3 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ _n) (ite (___z21z___ _n) 0 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_2 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) (+ 1 (+ ?v_3 ?v_0)) ?v_0) ?v_0)))))))))))
(assert (= (___z25z___ _n) (ite (= _n _base) (___z10z___ _n) (___z25z___ (+ _n (- 1))))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (___z26z___ _n))) (= (___z16z___ _n) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (___z16z___ (+ _n (- 1)))))))))
(assert (let ((?v_2 (___z9z___ _n)) (?v_0 (___z8z___ _n)) (?v_5 (___z7z___ _n)) (?v_14 (___z4z___ _n)) (?v_17 (___z3z___ _n)) (?v_19 (___z2z___ _n)) (?v_11 (___z5z___ _n)) (?v_8 (___z6z___ _n))) (let ((?v_3 (not ?v_2)) (?v_18 (not ?v_19)) (?v_20 (not ?v_17))) (let ((?v_15 (and ?v_20 ?v_18)) (?v_16 (not ?v_14))) (let ((?v_12 (and ?v_16 ?v_15)) (?v_13 (not ?v_11))) (let ((?v_9 (and ?v_13 ?v_12)) (?v_10 (not ?v_8))) (let ((?v_6 (and ?v_10 ?v_9)) (?v_7 (not ?v_5))) (let ((?v_1 (and ?v_7 ?v_6)) (?v_4 (not ?v_0))) (let ((?v_21 (and ?v_4 ?v_1))) (= (___z26z___ _n) (and (<= 0 (___z10z___ _n)) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3))))))))))))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z17z___ _n) (and (= (___z14z___ ?v_0) 0) (and (= (___z15z___ ?v_0) 0) (and (= (___z13z___ ?v_0) 0) (<= 1 (___z12z___ ?v_0))))))))
(assert (= (___z27z___ _n) (ite (= _n _base) (___z10z___ _n) (___z27z___ (+ _n (- 1))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z18z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (___z13z___ ?v_0))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z19z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (+ (___z14z___ ?v_0) (___z15z___ ?v_0)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (<= 1 (___z14z___ (+ (- 1) ?v_0))) (___z20z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (or (not (___z16z___ ?v_0)) (= (+ (___z14z___ ?v_0) (+ (___z15z___ ?v_0) (+ (___z12z___ ?v_0) (+ (___z13z___ ?v_0) (* (- 1) (___z27z___ ?v_0)))))) 0)) (___z11z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (= (___z15z___ (+ (- 1) ?v_0)) 1) (___z21z___ ?v_0))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z12z___ (+ (- 1) ?v_0)))) (let ((?v_2 (+ (- 1) ?v_1))) (= (___z12z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) (___z25z___ ?v_0) (ite (___z2z___ ?v_0) (ite (___z17z___ ?v_0) ?v_2 ?v_1) (ite (___z3z___ ?v_0) (ite (___z18z___ ?v_0) ?v_2 ?v_1) (ite (___z4z___ ?v_0) (ite (___z19z___ ?v_0) ?v_2 ?v_1) (ite (___z7z___ ?v_0) (ite (___z22z___ ?v_0) ?v_2 ?v_1) (ite (___z8z___ ?v_0) (ite (___z23z___ ?v_0) ?v_2 ?v_1) (ite (___z9z___ ?v_0) (ite (___z24z___ ?v_0) ?v_2 ?v_1) ?v_1))))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z22z___ ?v_0) (and (= (___z14z___ ?v_1) 0) (and (= (___z15z___ ?v_1) 0) (and (= (___z13z___ ?v_1) 0) (<= 1 (___z12z___ ?v_1)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z13z___ (+ (- 1) ?v_0)))) (let ((?v_2 (+ (- 1) ?v_1))) (= (___z13z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (___z3z___ ?v_0) (ite (___z18z___ ?v_0) ?v_2 ?v_1) (ite (___z5z___ ?v_0) (ite (___z20z___ ?v_0) (+ 1 ?v_1) ?v_1) (ite (___z7z___ ?v_0) (ite (___z22z___ ?v_0) 1 ?v_1) (ite (___z8z___ ?v_0) (ite (___z23z___ ?v_0) ?v_2 ?v_1) ?v_1))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z23z___ ?v_0) (and (<= 1 (___z12z___ ?v_1)) (<= 1 (___z13z___ ?v_1)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (___z14z___ (+ (- 1) ?v_0)))) (let ((?v_2 (+ 1 ?v_1))) (= (___z14z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (___z2z___ ?v_0) (ite (___z17z___ ?v_0) ?v_2 ?v_1) (ite (___z4z___ ?v_0) (ite (___z19z___ ?v_0) 0 ?v_1) (ite (___z5z___ ?v_0) (ite (___z20z___ ?v_0) (+ (- 1) ?v_1) ?v_1) (ite (___z6z___ ?v_0) (ite (___z21z___ ?v_0) ?v_2 ?v_1) (ite (___z9z___ ?v_0) (ite (___z24z___ ?v_0) 0 ?v_1) ?v_1)))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z24z___ ?v_0) (and (<= 1 (___z12z___ ?v_1)) (<= 1 (+ (___z14z___ ?v_1) (___z15z___ ?v_1))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_2 (+ (- 1) ?v_0))) (let ((?v_4 (___z14z___ ?v_2)) (?v_1 (___z15z___ ?v_2))) (let ((?v_3 (+ 2 ?v_1))) (= (___z15z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) 0 (ite (___z3z___ ?v_0) (ite (___z18z___ ?v_0) ?v_3 ?v_1) (ite (___z4z___ ?v_0) (ite (___z19z___ ?v_0) (+ (- 1) (+ ?v_4 (+ (- 1) ?v_1))) ?v_1) (ite (___z6z___ ?v_0) (ite (___z21z___ ?v_0) 0 ?v_1) (ite (___z8z___ ?v_0) (ite (___z23z___ ?v_0) ?v_3 ?v_1) (ite (___z9z___ ?v_0) (ite (___z24z___ ?v_0) (+ 1 (+ ?v_4 ?v_1)) ?v_1) ?v_1))))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z25z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) (___z10z___ ?v_0) (___z25z___ (+ (- 1) ?v_0))))))
(assert (let ((?v_0 (+ _n (- 1))) (?v_1 (= (+ _n (* (- 1) _base)) 1))) (let ((?v_2 (___z26z___ ?v_0))) (= (___z16z___ ?v_0) (and (or (not ?v_1) ?v_2) (or ?v_1 (and ?v_2 (___z16z___ (+ (- 1) ?v_0)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_20 (___z2z___ ?v_0)) (?v_18 (___z3z___ ?v_0)) (?v_15 (___z4z___ ?v_0)) (?v_6 (___z7z___ ?v_0)) (?v_1 (___z8z___ ?v_0)) (?v_3 (___z9z___ ?v_0)) (?v_12 (___z5z___ ?v_0)) (?v_9 (___z6z___ ?v_0))) (let ((?v_5 (not ?v_1)) (?v_8 (not ?v_6)) (?v_11 (not ?v_9)) (?v_14 (not ?v_12)) (?v_17 (not ?v_15)) (?v_21 (not ?v_18)) (?v_19 (not ?v_20))) (let ((?v_16 (and ?v_21 ?v_19))) (let ((?v_13 (and ?v_17 ?v_16))) (let ((?v_10 (and ?v_14 ?v_13))) (let ((?v_7 (and ?v_11 ?v_10))) (let ((?v_2 (and ?v_8 ?v_7))) (let ((?v_22 (and ?v_5 ?v_2)) (?v_4 (not ?v_3))) (= (___z26z___ ?v_0) (and (<= 0 (___z10z___ ?v_0)) (or (and ?v_3 ?v_22) (or (and (and ?v_1 ?v_2) ?v_4) (or (and ?v_4 (and ?v_5 (and ?v_6 ?v_7))) (or (and ?v_4 (and ?v_5 (and ?v_8 (and ?v_9 ?v_10)))) (or (and ?v_4 (and ?v_5 (and ?v_8 (and ?v_11 (and ?v_12 ?v_13))))) (or (and ?v_4 (and ?v_5 (and ?v_8 (and ?v_11 (and ?v_14 (and ?v_15 ?v_16)))))) (or (and ?v_4 (and ?v_5 (and ?v_8 (and ?v_11 (and ?v_14 (and ?v_17 (and ?v_18 ?v_19))))))) (or (and ?v_4 (and ?v_5 (and ?v_8 (and ?v_11 (and ?v_14 (and ?v_17 (and ?v_20 ?v_21))))))) (and ?v_22 ?v_4)))))))))))))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z17z___ ?v_0) (and (= (___z14z___ ?v_1) 0) (and (= (___z15z___ ?v_1) 0) (and (= (___z13z___ ?v_1) 0) (<= 1 (___z12z___ ?v_1)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z27z___ ?v_0) (ite (= (+ _n (* (- 1) _base)) 1) (___z10z___ ?v_0) (___z27z___ (+ (- 1) ?v_0))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z18z___ ?v_0) (and (<= 1 (___z12z___ ?v_1)) (<= 1 (___z13z___ ?v_1)))))))
(assert (let ((?v_0 (+ _n (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z19z___ ?v_0) (and (<= 1 (___z12z___ ?v_1)) (<= 1 (+ (___z14z___ ?v_1) (___z15z___ ?v_1))))))))
(assert (___z11z___ (+ _n (- 1))))
(assert (not (or (not (= _base (- 1))) (___z11z___ _n))))
(assert true)
(set-info :status sat)
(check-sat)
(pop 1)
(assert (___z11z___ (+ _n (- 1))))
(assert (___z11z___ (+ _n (- 2))))
(assert (= (<= 1 (___z14z___ (- 3))) (___z20z___ (- 2))))
(assert (= (___z11z___ (- 2)) (or (not (___z16z___ (- 2))) (= (+ (___z14z___ (- 2)) (+ (___z15z___ (- 2)) (+ (___z12z___ (- 2)) (+ (___z13z___ (- 2)) (* (- 1) (___z27z___ (- 2))))))) 0))))
(assert (= (= (___z15z___ (- 3)) 1) (___z21z___ (- 2))))
(assert (let ((?v_0 (___z12z___ (- 3)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ (- 2)) (ite (= _base (- 2)) (___z25z___ (- 2)) (ite (___z2z___ (- 2)) (ite (___z17z___ (- 2)) ?v_1 ?v_0) (ite (___z3z___ (- 2)) (ite (___z18z___ (- 2)) ?v_1 ?v_0) (ite (___z4z___ (- 2)) (ite (___z19z___ (- 2)) ?v_1 ?v_0) (ite (___z7z___ (- 2)) (ite (___z22z___ (- 2)) ?v_1 ?v_0) (ite (___z8z___ (- 2)) (ite (___z23z___ (- 2)) ?v_1 ?v_0) (ite (___z9z___ (- 2)) (ite (___z24z___ (- 2)) ?v_1 ?v_0) ?v_0)))))))))))
(assert (= (___z22z___ (- 2)) (and (= (___z14z___ (- 3)) 0) (and (= (___z15z___ (- 3)) 0) (and (= (___z13z___ (- 3)) 0) (<= 1 (___z12z___ (- 3))))))))
(assert (let ((?v_0 (___z13z___ (- 3)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ (- 2)) (ite (= _base (- 2)) 0 (ite (___z3z___ (- 2)) (ite (___z18z___ (- 2)) ?v_1 ?v_0) (ite (___z5z___ (- 2)) (ite (___z20z___ (- 2)) (+ 1 ?v_0) ?v_0) (ite (___z7z___ (- 2)) (ite (___z22z___ (- 2)) 1 ?v_0) (ite (___z8z___ (- 2)) (ite (___z23z___ (- 2)) ?v_1 ?v_0) ?v_0)))))))))
(assert (= (___z23z___ (- 2)) (and (<= 1 (___z12z___ (- 3))) (<= 1 (___z13z___ (- 3))))))
(assert (let ((?v_0 (___z14z___ (- 3)))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ (- 2)) (ite (= _base (- 2)) 0 (ite (___z2z___ (- 2)) (ite (___z17z___ (- 2)) ?v_1 ?v_0) (ite (___z4z___ (- 2)) (ite (___z19z___ (- 2)) 0 ?v_0) (ite (___z5z___ (- 2)) (ite (___z20z___ (- 2)) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ (- 2)) (ite (___z21z___ (- 2)) ?v_1 ?v_0) (ite (___z9z___ (- 2)) (ite (___z24z___ (- 2)) 0 ?v_0) ?v_0))))))))))
(assert (= (___z24z___ (- 2)) (and (<= 1 (___z12z___ (- 3))) (<= 1 (+ (___z14z___ (- 3)) (___z15z___ (- 3)))))))
(assert (let ((?v_2 (___z14z___ (- 3))) (?v_0 (___z15z___ (- 3)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ (- 2)) (ite (= _base (- 2)) 0 (ite (___z3z___ (- 2)) (ite (___z18z___ (- 2)) ?v_1 ?v_0) (ite (___z4z___ (- 2)) (ite (___z19z___ (- 2)) (+ (- 1) (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ (- 2)) (ite (___z21z___ (- 2)) 0 ?v_0) (ite (___z8z___ (- 2)) (ite (___z23z___ (- 2)) ?v_1 ?v_0) (ite (___z9z___ (- 2)) (ite (___z24z___ (- 2)) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0))))))))))
(assert (= (___z25z___ (- 2)) (ite (= _base (- 2)) (___z10z___ (- 2)) (___z25z___ (- 3)))))
(assert (let ((?v_0 (= _base (- 2))) (?v_1 (___z26z___ (- 2)))) (= (___z16z___ (- 2)) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (___z16z___ (- 3))))))))
(assert (let ((?v_19 (___z2z___ (- 2))) (?v_17 (___z3z___ (- 2))) (?v_14 (___z4z___ (- 2))) (?v_5 (___z7z___ (- 2))) (?v_0 (___z8z___ (- 2))) (?v_2 (___z9z___ (- 2))) (?v_11 (___z5z___ (- 2))) (?v_8 (___z6z___ (- 2)))) (let ((?v_4 (not ?v_0)) (?v_7 (not ?v_5)) (?v_10 (not ?v_8)) (?v_13 (not ?v_11)) (?v_16 (not ?v_14)) (?v_20 (not ?v_17)) (?v_18 (not ?v_19))) (let ((?v_15 (and ?v_20 ?v_18))) (let ((?v_12 (and ?v_16 ?v_15))) (let ((?v_9 (and ?v_13 ?v_12))) (let ((?v_6 (and ?v_10 ?v_9))) (let ((?v_1 (and ?v_7 ?v_6))) (let ((?v_21 (and ?v_4 ?v_1)) (?v_3 (not ?v_2))) (= (___z26z___ (- 2)) (and (<= 0 (___z10z___ (- 2))) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3))))))))))))))))))))
(assert (= (___z17z___ (- 2)) (and (= (___z14z___ (- 3)) 0) (and (= (___z15z___ (- 3)) 0) (and (= (___z13z___ (- 3)) 0) (<= 1 (___z12z___ (- 3))))))))
(assert (= (___z27z___ (- 2)) (ite (= _base (- 2)) (___z10z___ (- 2)) (___z27z___ (- 3)))))
(assert (= (___z18z___ (- 2)) (and (<= 1 (___z12z___ (- 3))) (<= 1 (___z13z___ (- 3))))))
(assert (= (___z19z___ (- 2)) (and (<= 1 (___z12z___ (- 3))) (<= 1 (+ (___z14z___ (- 3)) (___z15z___ (- 3)))))))
(assert (= (<= 1 (___z14z___ (+ _n (- 1)))) (___z20z___ _n)))
(assert (= (or (not (___z16z___ _n)) (= (+ (___z27z___ _n) (+ (* (- 1) (___z15z___ _n)) (+ (* (- 1) (___z14z___ _n)) (+ (* (- 1) (___z13z___ _n)) (* (- 1) (___z12z___ _n)))))) 0)) (___z11z___ _n)))
(assert (= (= (___z15z___ (+ _n (- 1))) 1) (___z21z___ _n)))
(assert (let ((?v_0 (___z12z___ (+ _n (- 1))))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ _n) (ite (= _n _base) (___z25z___ _n) (ite (___z2z___ _n) (ite (___z17z___ _n) ?v_1 ?v_0) (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_1 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) ?v_1 ?v_0) (ite (___z7z___ _n) (ite (___z22z___ _n) ?v_1 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_1 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) ?v_1 ?v_0) ?v_0)))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z22z___ _n) (and (= (___z14z___ ?v_0) 0) (and (= (___z15z___ ?v_0) 0) (and (= (___z13z___ ?v_0) 0) (<= 1 (___z12z___ ?v_0))))))))
(assert (let ((?v_0 (___z13z___ (+ _n (- 1))))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ _n) (ite (= _n _base) 0 (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_1 ?v_0) (ite (___z5z___ _n) (ite (___z20z___ _n) (+ 1 ?v_0) ?v_0) (ite (___z7z___ _n) (ite (___z22z___ _n) 1 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_1 ?v_0) ?v_0)))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z23z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (___z13z___ ?v_0))))))
(assert (let ((?v_0 (___z14z___ (+ _n (- 1))))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ _n) (ite (= _n _base) 0 (ite (___z2z___ _n) (ite (___z17z___ _n) ?v_1 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) 0 ?v_0) (ite (___z5z___ _n) (ite (___z20z___ _n) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ _n) (ite (___z21z___ _n) ?v_1 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) 0 ?v_0) ?v_0))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z24z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (+ (___z14z___ ?v_0) (___z15z___ ?v_0)))))))
(assert (let ((?v_1 (+ _n (- 1)))) (let ((?v_3 (___z14z___ ?v_1)) (?v_0 (___z15z___ ?v_1))) (let ((?v_2 (+ 2 ?v_0))) (= (___z15z___ _n) (ite (= _n _base) 0 (ite (___z3z___ _n) (ite (___z18z___ _n) ?v_2 ?v_0) (ite (___z4z___ _n) (ite (___z19z___ _n) (+ (- 1) (+ ?v_3 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ _n) (ite (___z21z___ _n) 0 ?v_0) (ite (___z8z___ _n) (ite (___z23z___ _n) ?v_2 ?v_0) (ite (___z9z___ _n) (ite (___z24z___ _n) (+ 1 (+ ?v_3 ?v_0)) ?v_0) ?v_0)))))))))))
(assert (= (___z25z___ _n) (ite (= _n _base) (___z10z___ _n) (___z25z___ (+ _n (- 1))))))
(assert (let ((?v_0 (= _n _base)) (?v_1 (___z26z___ _n))) (= (___z16z___ _n) (and (or (not ?v_0) ?v_1) (or ?v_0 (and ?v_1 (___z16z___ (+ _n (- 1)))))))))
(assert (let ((?v_2 (___z9z___ _n)) (?v_0 (___z8z___ _n)) (?v_5 (___z7z___ _n)) (?v_14 (___z4z___ _n)) (?v_17 (___z3z___ _n)) (?v_19 (___z2z___ _n)) (?v_11 (___z5z___ _n)) (?v_8 (___z6z___ _n))) (let ((?v_3 (not ?v_2)) (?v_18 (not ?v_19)) (?v_20 (not ?v_17))) (let ((?v_15 (and ?v_20 ?v_18)) (?v_16 (not ?v_14))) (let ((?v_12 (and ?v_16 ?v_15)) (?v_13 (not ?v_11))) (let ((?v_9 (and ?v_13 ?v_12)) (?v_10 (not ?v_8))) (let ((?v_6 (and ?v_10 ?v_9)) (?v_7 (not ?v_5))) (let ((?v_1 (and ?v_7 ?v_6)) (?v_4 (not ?v_0))) (let ((?v_21 (and ?v_4 ?v_1))) (= (___z26z___ _n) (and (<= 0 (___z10z___ _n)) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3))))))))))))))))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z17z___ _n) (and (= (___z14z___ ?v_0) 0) (and (= (___z15z___ ?v_0) 0) (and (= (___z13z___ ?v_0) 0) (<= 1 (___z12z___ ?v_0))))))))
(assert (= (___z27z___ _n) (ite (= _n _base) (___z10z___ _n) (___z27z___ (+ _n (- 1))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z18z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (___z13z___ ?v_0))))))
(assert (let ((?v_0 (+ _n (- 1)))) (= (___z19z___ _n) (and (<= 1 (___z12z___ ?v_0)) (<= 1 (+ (___z14z___ ?v_0) (___z15z___ ?v_0)))))))
(push 1)
(assert (not (or (___z11z___ 0) (not (= _base (- 2))))))
(assert true)
(set-info :status sat)
(check-sat)
(exit)
